Left Termination proof of /tmp/tmpuGgQKc/vangelder.pl

Left Termination of the query pattern q_in_2(g, g) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

e(a, b).
q(X, Y) :- e(X, Y).
q(X, f(f(X))) :- ','(p(X, f(f(X))), q(X, f(X))).
q(X, f(f(Y))) :- p(X, f(Y)).
p(X, Y) :- e(X, Y).
p(X, f(Y)) :- ','(r(X, f(Y)), p(X, Y)).
r(X, Y) :- e(X, Y).
r(X, f(Y)) :- ','(q(X, Y), r(X, Y)).
r(f(X), f(X)) :- t(f(X), f(X)).
t(X, Y) :- e(X, Y).
t(f(X), f(Y)) :- ','(q(f(X), f(Y)), t(X, Y)).

Queries:

q(g,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
q_in: (b,b)
p_in: (b,b)
r_in: (b,b)
t_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2) = q_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x3)
e_in_gg(x1, x2) = e_in_gg(x1, x2)
a = a
b = b
e_out_gg(x1, x2) = e_out_gg
q_out_gg(x1, x2) = q_out_gg
f(x1) = f(x1)
U2_gg(x1, x2) = U2_gg(x1, x2)
p_in_gg(x1, x2) = p_in_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x3)
p_out_gg(x1, x2) = p_out_gg
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
r_in_gg(x1, x2) = r_in_gg(x1, x2)
U8_gg(x1, x2, x3) = U8_gg(x3)
r_out_gg(x1, x2) = r_out_gg
U9_gg(x1, x2, x3) = U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3) = U4_gg(x3)
U10_gg(x1, x2, x3) = U10_gg(x3)
U11_gg(x1, x2) = U11_gg(x2)
t_in_gg(x1, x2) = t_in_gg(x1, x2)
U12_gg(x1, x2, x3) = U12_gg(x3)
t_out_gg(x1, x2) = t_out_gg
U13_gg(x1, x2, x3) = U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3) = U14_gg(x3)
U7_gg(x1, x2, x3) = U7_gg(x3)
U3_gg(x1, x2) = U3_gg(x2)
U5_GG(x1, x2, x3) = U5_GG(x3)
U4_GG(x1, x2, x3) = U4_GG(x3)
R_IN_GG(x1, x2) = R_IN_GG(x1, x2)
U11_GG(x1, x2) = U11_GG(x2)
P_IN_GG(x1, x2) = P_IN_GG(x1, x2)
Q_IN_GG(x1, x2) = Q_IN_GG(x1, x2)
U2_GG(x1, x2) = U2_GG(x1, x2)
U3_GG(x1, x2) = U3_GG(x2)
U12_GG(x1, x2, x3) = U12_GG(x3)
E_IN_GG(x1, x2) = E_IN_GG(x1, x2)
U6_GG(x1, x2, x3) = U6_GG(x1, x2, x3)
U13_GG(x1, x2, x3) = U13_GG(x1, x2, x3)
U1_GG(x1, x2, x3) = U1_GG(x3)
U9_GG(x1, x2, x3) = U9_GG(x1, x2, x3)
U10_GG(x1, x2, x3) = U10_GG(x3)
U14_GG(x1, x2, x3) = U14_GG(x3)
T_IN_GG(x1, x2) = T_IN_GG(x1, x2)
U7_GG(x1, x2, x3) = U7_GG(x3)
U8_GG(x1, x2, x3) = U8_GG(x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2) = q_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x3)
e_in_gg(x1, x2) = e_in_gg(x1, x2)
a = a
b = b
e_out_gg(x1, x2) = e_out_gg
q_out_gg(x1, x2) = q_out_gg
f(x1) = f(x1)
U2_gg(x1, x2) = U2_gg(x1, x2)
p_in_gg(x1, x2) = p_in_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x3)
p_out_gg(x1, x2) = p_out_gg
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
r_in_gg(x1, x2) = r_in_gg(x1, x2)
U8_gg(x1, x2, x3) = U8_gg(x3)
r_out_gg(x1, x2) = r_out_gg
U9_gg(x1, x2, x3) = U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3) = U4_gg(x3)
U10_gg(x1, x2, x3) = U10_gg(x3)
U11_gg(x1, x2) = U11_gg(x2)
t_in_gg(x1, x2) = t_in_gg(x1, x2)
U12_gg(x1, x2, x3) = U12_gg(x3)
t_out_gg(x1, x2) = t_out_gg
U13_gg(x1, x2, x3) = U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3) = U14_gg(x3)
U7_gg(x1, x2, x3) = U7_gg(x3)
U3_gg(x1, x2) = U3_gg(x2)
R_IN_GG(x1, x2) = R_IN_GG(x1, x2)
P_IN_GG(x1, x2) = P_IN_GG(x1, x2)
Q_IN_GG(x1, x2) = Q_IN_GG(x1, x2)
U2_GG(x1, x2) = U2_GG(x1, x2)
U6_GG(x1, x2, x3) = U6_GG(x1, x2, x3)
U13_GG(x1, x2, x3) = U13_GG(x1, x2, x3)
U9_GG(x1, x2, x3) = U9_GG(x1, x2, x3)
T_IN_GG(x1, x2) = T_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))

The remaining pairs can at least be oriented weakly.

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

Used ordering: Polynomial interpretation [25]:

POL(P_IN_GG(x₁, x₂)) = x₁
POL(Q_IN_GG(x₁, x₂)) = x₁
POL(R_IN_GG(x₁, x₂)) = x₁
POL(T_IN_GG(x₁, x₂)) = x₁
POL(U10_gg(x₁)) = 0
POL(U11_gg(x₁)) = 0
POL(U12_gg(x₁)) = 0
POL(U13_GG(x₁, x₂, x₃)) = x₁
POL(U13_gg(x₁, x₂, x₃)) = 0
POL(U14_gg(x₁)) = 0
POL(U1_gg(x₁)) = 0
POL(U2_GG(x₁, x₂)) = x₁
POL(U2_gg(x₁, x₂)) = 0
POL(U3_gg(x₁)) = 0
POL(U4_gg(x₁)) = 0
POL(U5_gg(x₁)) = 0
POL(U6_GG(x₁, x₂, x₃)) = x₁
POL(U6_gg(x₁, x₂, x₃)) = 0
POL(U7_gg(x₁)) = 0
POL(U8_gg(x₁)) = 0
POL(U9_GG(x₁, x₂, x₃)) = x₁
POL(U9_gg(x₁, x₂, x₃)) = 0
POL(a) = 0
POL(b) = 0
POL(e_in_gg(x₁, x₂)) = 0
POL(e_out_gg) = 0
POL(f(x₁)) = 1 + x₁
POL(p_in_gg(x₁, x₂)) = 0
POL(p_out_gg) = 0
POL(q_in_gg(x₁, x₂)) = 0
POL(q_out_gg) = 0
POL(r_in_gg(x₁, x₂)) = x₁
POL(r_out_gg) = 0
POL(t_in_gg(x₁, x₂)) = 0
POL(t_out_gg) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y)) we obtained the following new rules:

T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Instantiation

                            ↳ QDP

                              ↳ QDPOrderProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The remaining pairs can at least be oriented weakly.

U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

Used ordering: Polynomial interpretation [25]:

POL(P_IN_GG(x₁, x₂)) = x₂
POL(Q_IN_GG(x₁, x₂)) = x₂
POL(R_IN_GG(x₁, x₂)) = x₂
POL(T_IN_GG(x₁, x₂)) = x₂
POL(U10_gg(x₁)) = 0
POL(U11_gg(x₁)) = 0
POL(U12_gg(x₁)) = 0
POL(U13_gg(x₁, x₂, x₃)) = 0
POL(U14_gg(x₁)) = 0
POL(U1_gg(x₁)) = 0
POL(U2_GG(x₁, x₂)) = 1 + x₁
POL(U2_gg(x₁, x₂)) = 0
POL(U3_gg(x₁)) = 0
POL(U4_gg(x₁)) = 0
POL(U5_gg(x₁)) = 0
POL(U6_GG(x₁, x₂, x₃)) = x₂
POL(U6_gg(x₁, x₂, x₃)) = 0
POL(U7_gg(x₁)) = 0
POL(U8_gg(x₁)) = 0
POL(U9_GG(x₁, x₂, x₃)) = x₂
POL(U9_gg(x₁, x₂, x₃)) = 0
POL(a) = 0
POL(b) = 0
POL(e_in_gg(x₁, x₂)) = 0
POL(e_out_gg) = 0
POL(f(x₁)) = 1 + x₁
POL(p_in_gg(x₁, x₂)) = 0
POL(p_out_gg) = 0
POL(q_in_gg(x₁, x₂)) = 0
POL(q_out_gg) = 0
POL(r_in_gg(x₁, x₂)) = 0
POL(r_out_gg) = 0
POL(t_in_gg(x₁, x₂)) = 0
POL(t_out_gg) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Instantiation

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 7 less nodes.
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
q_in: (b,b)
p_in: (b,b)
r_in: (b,b)
t_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 14 less nodes.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))

The remaining pairs can at least be oriented weakly.

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

Used ordering: Polynomial interpretation [25]:

POL(P_IN_GG(x₁, x₂)) = x₁
POL(Q_IN_GG(x₁, x₂)) = x₁
POL(R_IN_GG(x₁, x₂)) = x₁
POL(T_IN_GG(x₁, x₂)) = x₁
POL(U10_gg(x₁, x₂, x₃)) = 0
POL(U11_gg(x₁, x₂)) = 0
POL(U12_gg(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U13_GG(x₁, x₂, x₃)) = x₁
POL(U13_gg(x₁, x₂, x₃)) = 0
POL(U14_gg(x₁, x₂, x₃)) = 0
POL(U1_gg(x₁, x₂, x₃)) = x₃
POL(U2_GG(x₁, x₂)) = x₁
POL(U2_gg(x₁, x₂)) = 0
POL(U3_gg(x₁, x₂)) = 0
POL(U4_gg(x₁, x₂, x₃)) = 0
POL(U5_gg(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U6_GG(x₁, x₂, x₃)) = x₁
POL(U6_gg(x₁, x₂, x₃)) = 0
POL(U7_gg(x₁, x₂, x₃)) = 0
POL(U8_gg(x₁, x₂, x₃)) = x₃
POL(U9_GG(x₁, x₂, x₃)) = x₁
POL(U9_gg(x₁, x₂, x₃)) = 0
POL(a) = 0
POL(b) = 0
POL(e_in_gg(x₁, x₂)) = 0
POL(e_out_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(f(x₁)) = 1 + x₁
POL(p_in_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(p_out_gg(x₁, x₂)) = x₂
POL(q_in_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(q_out_gg(x₁, x₂)) = 0
POL(r_in_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(r_out_gg(x₁, x₂)) = 0
POL(t_in_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(t_out_gg(x₁, x₂)) = 1 + x₁ + x₂

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y)) we obtained the following new rules:

T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ Instantiation

                            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0, x1, x2)
p_in_gg(x0, x1)
U5_gg(x0, x1, x2)
r_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U4_gg(x0, x1, x2)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0, x1, x2)
U13_gg(x0, x1, x2)
U14_gg(x0, x1, x2)
U11_gg(x0, x1)
U10_gg(x0, x1, x2)
U6_gg(x0, x1, x2)
U7_gg(x0, x1, x2)
U2_gg(x0, x1)
U3_gg(x0, x1)

We have to consider all (P,Q,R)-chains.